1. Field of the Invention
This invention relates to the design and verification of hardware systems, such as digital integrated circuits. More specifically, this invention relates to a method for generating a set of assertions of a hardware design that are true for a trace, where the trace is based on a sequence of design inputs.
2. Description of the Related Art
An electronic design automation (EDA) system is a form of computer aided design (CAD) system used for designing hardware systems such as integrated circuit (IC) devices. FIG. 1 illustrates a process for electronic design automation. The EDA system typically receives one or more high level behavioral descriptions of hardware design (see step 101) (e.g. in hardware description languages like VHDL, Verilog, etc.) and translates this high level design language description into netlists of various levels of abstraction, including nodes and edges (see step 102). At a higher level of abstraction, a generic netlist is typically produced based on library primitives. The generic netlist can be translated into a lower level technology-specific netlist based on a technology-specific library. A netlist describes the IC design and is composed of nodes (also referred to as design elements) and edges, e.g., connections between nodes, and can be represented using a directed cyclic graph structure having nodes which are connected to each other. The netlist is typically stored in computer readable media (also referred to as a computer readable storage medium) within the EDA system and optimized, verified and otherwise processed using many well known techniques (see step 103). The netlist may then be used to generate a physical device layout in mask form at step 104. The layout can be used to directly implement structures in silicon to realize the physical IC device at step 105.
At several points in the design process, it is useful to be able to simulate and verify the design, or parts of the design, to verify that it operates logically as desired. If errors are found, then the design is modified or corrected in iterative fashion as necessary. Several methods are known for verifying circuit designs. In one method, software models of the design are created and the software models are tested against designer-specified test cases. In other methods, each component in the design is modeled as a state transition system and described using logical formulas. All possible behaviors of the circuit design are then exercised to confirm that the design performs in accordance with the state transition logical formulas. The latter methods are more exhaustive than the former, but can require large amounts of time and computing power to generate and execute.
A design verification methodology, known as assertion-based verification, involves testing a simulation of the circuit against one or more assertions describing how the circuit should behave. An “assertion” is a statement that captures the intended behavior of a hardware design. For example, a request must always be followed by a grant within two clock cycles. Assertions allow for automated checking that the specified property is true, and can generate automatic error messages if the property is not true. Industry organizations have defined standardized assertion languages that designers can use to specify their assertions, and for which tool vendors have developed automated checking tools.
An assertion typically relates the values of one or more design elements in a hardware design at one or more time instances. Assertions can be viewed as declarative specifications of the underlying hardware design. An assertion failure indicates an error or a bug of the hardware design. Assertions have been widely used in both hardware designs and software designs to aid design, verification and debugging.
In main stream design and verification methodologies, engineers write assertions manually. A large design often contains thousands of assertions. Manual creation of assertions is time consuming and error prone.
Existing approaches for automatically generating of assertion can be divided into two categories. Approaches in the first category are similar to software linting tools. Syntactical analysis is the key to such approaches. Assertions are generated based on pre-defined patterns in the syntax of HDL descriptions, such as one-hot encoding; or based on comments that users have written, such as full case and parallel case pragmas; or based on particular constructs of a hardware design, such as latch inference or clock-domain crossing. These lint-like approaches have a number of drawbacks. The analysis is based on syntactical structure of HDL descriptions, and it does not “understand” the actual functionality or the semantics of a design. As a consequence, assertions generated in this approach often fail to capture the real functional behaviors of the design and miss bugs. These approaches also produce many false warning messages.
Approaches in the second category are based on trial-and-error. More specifically, in these approaches, a set of candidate assertions are enumerated and tested against simulation traces, and the assertions that passed the simulation traces are presented as design assertions. The problem with such brute-force approaches is inefficiency—the space of candidate assertions is simply too vast to test through long simulation traces. In practice, these approaches generate candidate assertions based on some limited and pre-defined patterns, such as mutual exclusion or request and acknowledgment pairs. As a consequence, these approaches fail to generate useful assertions that do not fit the pre-defined patterns. Even for the pre-defined patterns, these approaches are often too slow for practical designs.
Hence, a method and an apparatus for automatically and efficiently generating assertions is needed that can capture general behaviors, including temporal behaviors, of design elements in a hardware design.